Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(app(const,x),y)	→ x
2:		app(app(app(subst,f),g),x)	→ app(app(f,x),app(g,x))
3:		app(app(fix,f),x)	→ app(app(f,app(fix,f)),x)

There are 5 dependency pairs:


4:		APP(app(app(subst,f),g),x)	→ APP(app(f,x),app(g,x))
5:		APP(app(app(subst,f),g),x)	→ APP(f,x)
6:		APP(app(app(subst,f),g),x)	→ APP(g,x)
7:		APP(app(fix,f),x)	→ APP(app(f,app(fix,f)),x)
8:		APP(app(fix,f),x)	→ APP(f,app(fix,f))

Consider the SCC {4-8}. The constraints could not be solved.

Tyrolean Termination Tool (0.03 seconds) --- May 4, 2006